perm filename MARS1.PRF[PRF,JRA] blob sn#005926 filedate 1972-10-06 generic text, type T, neo UTF8
STRATEGY =
(LAMBDA (X) (SUPPORT X)) 
SUPPORT-SET-IS: 
¬=(/(1,/(THM52,THM53)),1) 
UNIT-PREFERENCE =NIL
MERGE =NIL
ORDER =NIL
ANCESTRY =T
DEPTH-BOUND =3
LENGTH-BOUND =2

PARMODULATE =T
EQUAL-SYMBOL ==
PAR-DEPTH-BOUND =3
ELAPSED-TIME =3467

NIL 1 2
1 ¬=(/(X1,THM53),0) 3 4
2 =(/(0,X1),0) HYP 5
3 ²(X1,THM53) 5 6
4 ≤(X1,X1) ¬=(/(X2,X1),0) AX 3
5 =(/(X1,X2),0) ²(X1,X2) AX 2
6 ¬=(/(1,/(THM52,THM53)),1) THM 2